Termination Proof Script

Consider the TRS R consisting of the rewrite rule


1:	app(app(app(compose,f),g),x)	→ app(f,app(g,x))

There are 2 dependency pairs:


2:	APP(app(app(compose,f),g),x)	→ APP(f,app(g,x))
3:	APP(app(app(compose,f),g),x)	→ APP(g,x)

Consider the SCC {2,3}. By taking the AF π with π(APP) = 1 together with the lexicographic path order with empty precedence, the rules in {1-3} are strictly decreasing. Hence the TRS is terminating.

Tyrolean Termination Tool (0.01 seconds) --- May 3, 2006